H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 2.178 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule Main

((significand :: Float -> Float) :: Float -> Float)

module Main where

import qualified Prelude

Lambda Reductions:
The following Lambda expression

\(m,_)→m

is transformed to

m0 (m,_) = m

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule Main

((significand :: Float -> Float) :: Float -> Float)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule Main

((significand :: Float -> Float) :: Float -> Float)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

power vw 0 = 1.0

power x vx@(y+1) = fromInt x * power x y

power x y = 1.0 / power x (`negate` y)

is transformed to

power vw xw = power4 vw xw

power x vx = power2 x vx

power x y = power0 x y

power0 x y = 1.0 / power x (`negate` y)

power1 True x vx = fromInt x * power x (vx - 1)

power1 wx wy wz = power0 wy wz

power2 x vx = power1 (vx >= 1) x vx

power2 xu xv = power0 xu xv

power3 True vw xw = 1.0

power3 xx xy xz = power2 xy xz

power4 vw xw = power3 (xw == 0) vw xw

power4 yu yv = power2 yu yv

The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

mainModule Main

((significand :: Float -> Float) :: Float -> Float)

module Main where

import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

encodeFloat m (`negate` floatDigits x)

where

m = m0 vu11

m0 (m,vv) = m

vu11 = decodeFloat x

are unpacked to the following functions on top level

significandM0 yw (m,vv) = m

significandM yw = significandM0 yw (significandVu11 yw)

significandVu11 yw = decodeFloat yw

The bindings of the following Let/Where expression

fromInteger x * power 2 y

where

power vw xw = power4 vw xw

power x vx = power2 x vx

power x y = power0 x y

power0 x y = 1.0 / power x (`negate` y)

power1 True x vx = fromInt x * power x (vx - 1)

power1 wx wy wz = power0 wy wz

power2 x vx = power1 (vx >= 1) x vx

power2 xu xv = power0 xu xv

power3 True vw xw = 1.0

power3 xx xy xz = power2 xy xz

power4 vw xw = power3 (xw == 0) vw xw

power4 yu yv = power2 yu yv

are unpacked to the following functions on top level

primFloatEncodePower4 vw xw = primFloatEncodePower3 (xw == 0) vw xw

primFloatEncodePower4 yu yv = primFloatEncodePower2 yu yv

primFloatEncodePower1 True x vx = fromInt x * primFloatEncodePower x (vx - 1)

primFloatEncodePower1 wx wy wz = primFloatEncodePower0 wy wz

primFloatEncodePower3 True vw xw = 1.0

primFloatEncodePower3 xx xy xz = primFloatEncodePower2 xy xz

primFloatEncodePower vw xw = primFloatEncodePower4 vw xw

primFloatEncodePower x vx = primFloatEncodePower2 x vx

primFloatEncodePower x y = primFloatEncodePower0 x y

primFloatEncodePower2 x vx = primFloatEncodePower1 (vx >= 1) x vx

primFloatEncodePower2 xu xv = primFloatEncodePower0 xu xv

primFloatEncodePower0 x y = 1.0 / primFloatEncodePower x (`negate` y)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

mainModule Main

((significand :: Float -> Float) :: Float -> Float)

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

mainModule Main

(significand :: Float -> Float)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="significand",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="significand yx3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="encodeFloat (significandM yx3) (`negate` floatDigits yx3)",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="primFloatEncode (significandM yx3) (`negate` floatDigits yx3)",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="fromInteger (significandM yx3) * primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` floatDigits yx3)",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="primMulFloat (fromInteger (significandM yx3)) (primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` floatDigits yx3))",fontsize=16,color="black",shape="box"];7 -> 8[label="",style="solid", color="black", weight=3];
8[label="primMulFloat (primIntegerToFloat (significandM yx3)) (primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` floatDigits yx3))",fontsize=16,color="black",shape="box"];8 -> 9[label="",style="solid", color="black", weight=3];
9 -> 14[label="",style="dashed", color="red", weight=0];
9[label="primMulFloat (primIntegerToFloat (significandM0 yx3 (significandVu11 yx3))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` floatDigits yx3))",fontsize=16,color="magenta"];9 -> 15[label="",style="dashed", color="magenta", weight=3];
15[label="significandVu11 yx3",fontsize=16,color="black",shape="box"];15 -> 20[label="",style="solid", color="black", weight=3];
14[label="primMulFloat (primIntegerToFloat (significandM0 yx3 yx4)) (primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` floatDigits yx3))",fontsize=16,color="burlywood",shape="triangle"];1197[label="yx4/(yx40,yx41)",fontsize=10,color="white",style="solid",shape="box"];14 -> 1197[label="",style="solid", color="burlywood", weight=9];
1197 -> 21[label="",style="solid", color="burlywood", weight=3];
20[label="decodeFloat yx3",fontsize=16,color="black",shape="box"];20 -> 23[label="",style="solid", color="black", weight=3];
21[label="primMulFloat (primIntegerToFloat (significandM0 yx3 (yx40,yx41))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` floatDigits yx3))",fontsize=16,color="black",shape="box"];21 -> 24[label="",style="solid", color="black", weight=3];
23[label="primFloatDecode yx3",fontsize=16,color="black",shape="box"];23 -> 25[label="",style="solid", color="black", weight=3];
24[label="primMulFloat (primIntegerToFloat yx40) (primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` floatDigits yx3))",fontsize=16,color="burlywood",shape="box"];1198[label="yx40/Integer yx400",fontsize=10,color="white",style="solid",shape="box"];24 -> 1198[label="",style="solid", color="burlywood", weight=9];
1198 -> 26[label="",style="solid", color="burlywood", weight=3];
25[label="terminator yx3",fontsize=16,color="black",shape="box"];25 -> 27[label="",style="solid", color="black", weight=3];
26[label="primMulFloat (primIntegerToFloat (Integer yx400)) (primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` floatDigits yx3))",fontsize=16,color="black",shape="box"];26 -> 28[label="",style="solid", color="black", weight=3];
27[label="ter1m yx3",fontsize=16,color="green",shape="box"];27 -> 29[label="",style="dashed", color="green", weight=3];
28[label="primMulFloat (primIntToFloat yx400) (primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` floatDigits yx3))",fontsize=16,color="black",shape="box"];28 -> 30[label="",style="solid", color="black", weight=3];
29[label="yx3",fontsize=16,color="green",shape="box"];30[label="primMulFloat (Float yx400 (Pos (Succ Zero))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` floatDigits yx3))",fontsize=16,color="black",shape="box"];30 -> 31[label="",style="solid", color="black", weight=3];
31[label="primMulFloat (Float yx400 (Pos (Succ Zero))) (primFloatEncodePower4 (Pos (Succ (Succ Zero))) (`negate` floatDigits yx3))",fontsize=16,color="black",shape="box"];31 -> 32[label="",style="solid", color="black", weight=3];
32[label="primMulFloat (Float yx400 (Pos (Succ Zero))) (primFloatEncodePower3 (`negate` floatDigits yx3 == Pos Zero) (Pos (Succ (Succ Zero))) (`negate` floatDigits yx3))",fontsize=16,color="black",shape="box"];32 -> 33[label="",style="solid", color="black", weight=3];
33[label="primMulFloat (Float yx400 (Pos (Succ Zero))) (primFloatEncodePower3 (primEqInt (`negate` floatDigits yx3) (Pos Zero)) (Pos (Succ (Succ Zero))) (`negate` floatDigits yx3))",fontsize=16,color="black",shape="box"];33 -> 34[label="",style="solid", color="black", weight=3];
34[label="primMulFloat (Float yx400 (Pos (Succ Zero))) (primFloatEncodePower3 (primEqInt (primNegInt (floatDigits yx3)) (Pos Zero)) (Pos (Succ (Succ Zero))) (primNegInt (floatDigits yx3)))",fontsize=16,color="black",shape="box"];34 -> 35[label="",style="solid", color="black", weight=3];
35[label="primMulFloat (Float yx400 (Pos (Succ Zero))) (primFloatEncodePower3 (primEqInt (primNegInt primFloatDigits) (Pos Zero)) (Pos (Succ (Succ Zero))) (primNegInt primFloatDigits))",fontsize=16,color="black",shape="box"];35 -> 36[label="",style="solid", color="black", weight=3];
36 -> 37[label="",style="dashed", color="red", weight=0];
36[label="primMulFloat (Float yx400 (Pos (Succ Zero))) (primFloatEncodePower3 (primEqInt (primNegInt (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))) (Pos Zero)) (Pos (Succ (Succ Zero))) (primNegInt (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))",fontsize=16,color="magenta"];36 -> 38[label="",style="dashed", color="magenta", weight=3];
36 -> 39[label="",style="dashed", color="magenta", weight=3];
38[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))",fontsize=16,color="green",shape="box"];39[label="yx400",fontsize=16,color="green",shape="box"];37[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (primFloatEncodePower3 (primEqInt (primNegInt (Pos (Succ yx7))) (Pos Zero)) (Pos (Succ (Succ Zero))) (primNegInt (Pos (Succ yx7))))",fontsize=16,color="black",shape="triangle"];37 -> 40[label="",style="solid", color="black", weight=3];
40[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (primFloatEncodePower3 (primEqInt (Neg (Succ yx7)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg (Succ yx7)))",fontsize=16,color="black",shape="box"];40 -> 41[label="",style="solid", color="black", weight=3];
41[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (primFloatEncodePower3 False (Pos (Succ (Succ Zero))) (Neg (Succ yx7)))",fontsize=16,color="black",shape="box"];41 -> 42[label="",style="solid", color="black", weight=3];
42[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (primFloatEncodePower2 (Pos (Succ (Succ Zero))) (Neg (Succ yx7)))",fontsize=16,color="black",shape="box"];42 -> 43[label="",style="solid", color="black", weight=3];
43[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (primFloatEncodePower1 (Neg (Succ yx7) >= Pos (Succ Zero)) (Pos (Succ (Succ Zero))) (Neg (Succ yx7)))",fontsize=16,color="black",shape="box"];43 -> 44[label="",style="solid", color="black", weight=3];
44[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (primFloatEncodePower1 (compare (Neg (Succ yx7)) (Pos (Succ Zero)) /= LT) (Pos (Succ (Succ Zero))) (Neg (Succ yx7)))",fontsize=16,color="black",shape="box"];44 -> 45[label="",style="solid", color="black", weight=3];
45[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (primFloatEncodePower1 (not (compare (Neg (Succ yx7)) (Pos (Succ Zero)) == LT)) (Pos (Succ (Succ Zero))) (Neg (Succ yx7)))",fontsize=16,color="black",shape="box"];45 -> 46[label="",style="solid", color="black", weight=3];
46[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (primFloatEncodePower1 (not (primCmpInt (Neg (Succ yx7)) (Pos (Succ Zero)) == LT)) (Pos (Succ (Succ Zero))) (Neg (Succ yx7)))",fontsize=16,color="black",shape="box"];46 -> 47[label="",style="solid", color="black", weight=3];
47[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (primFloatEncodePower1 (not (LT == LT)) (Pos (Succ (Succ Zero))) (Neg (Succ yx7)))",fontsize=16,color="black",shape="box"];47 -> 48[label="",style="solid", color="black", weight=3];
48[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (primFloatEncodePower1 (not True) (Pos (Succ (Succ Zero))) (Neg (Succ yx7)))",fontsize=16,color="black",shape="box"];48 -> 49[label="",style="solid", color="black", weight=3];
49[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (primFloatEncodePower1 False (Pos (Succ (Succ Zero))) (Neg (Succ yx7)))",fontsize=16,color="black",shape="box"];49 -> 50[label="",style="solid", color="black", weight=3];
50[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (primFloatEncodePower0 (Pos (Succ (Succ Zero))) (Neg (Succ yx7)))",fontsize=16,color="black",shape="box"];50 -> 51[label="",style="solid", color="black", weight=3];
51[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (fromDouble (Double (Pos (Succ Zero)) (Pos (Succ Zero))) / primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx7)))",fontsize=16,color="black",shape="box"];51 -> 52[label="",style="solid", color="black", weight=3];
52[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (primDivFloat (fromDouble (Double (Pos (Succ Zero)) (Pos (Succ Zero)))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx7))))",fontsize=16,color="black",shape="box"];52 -> 53[label="",style="solid", color="black", weight=3];
53[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (primDivFloat (doubleToFloat (Double (Pos (Succ Zero)) (Pos (Succ Zero)))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx7))))",fontsize=16,color="black",shape="box"];53 -> 54[label="",style="solid", color="black", weight=3];
54 -> 616[label="",style="dashed", color="red", weight=0];
54[label="primMulFloat (Float yx6 (Pos (Succ Zero))) (primDivFloat (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx7))))",fontsize=16,color="magenta"];54 -> 617[label="",style="dashed", color="magenta", weight=3];
54 -> 618[label="",style="dashed", color="magenta", weight=3];
617[label="yx6",fontsize=16,color="green",shape="box"];618[label="primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx7))",fontsize=16,color="black",shape="box"];618 -> 999[label="",style="solid", color="black", weight=3];
616[label="primMulFloat (Float yx26 (Pos (Succ Zero))) (primDivFloat (Float (Pos (Succ Zero)) (Pos (Succ Zero))) yx27)",fontsize=16,color="burlywood",shape="triangle"];1201[label="yx27/Float yx270 yx271",fontsize=10,color="white",style="solid",shape="box"];616 -> 1201[label="",style="solid", color="burlywood", weight=9];
1201 -> 1000[label="",style="solid", color="burlywood", weight=3];
999[label="primFloatEncodePower4 (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx7))",fontsize=16,color="black",shape="box"];999 -> 1001[label="",style="solid", color="black", weight=3];
1000[label="primMulFloat (Float yx26 (Pos (Succ Zero))) (primDivFloat (Float (Pos (Succ Zero)) (Pos (Succ Zero))) (Float yx270 yx271))",fontsize=16,color="black",shape="box"];1000 -> 1002[label="",style="solid", color="black", weight=3];
1001[label="primFloatEncodePower3 (`negate` Neg (Succ yx7) == Pos Zero) (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx7))",fontsize=16,color="black",shape="box"];1001 -> 1003[label="",style="solid", color="black", weight=3];
1002[label="primMulFloat (Float yx26 (Pos (Succ Zero))) (Float (Pos (Succ Zero) * yx271) (Pos (Succ Zero) * yx270))",fontsize=16,color="black",shape="box"];1002 -> 1004[label="",style="solid", color="black", weight=3];
1003[label="primFloatEncodePower3 (primEqInt (`negate` Neg (Succ yx7)) (Pos Zero)) (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx7))",fontsize=16,color="black",shape="box"];1003 -> 1005[label="",style="solid", color="black", weight=3];
1004[label="Float (yx26 * (Pos (Succ Zero) * yx271)) (Pos (Succ Zero) * (Pos (Succ Zero) * yx270))",fontsize=16,color="green",shape="box"];1004 -> 1006[label="",style="dashed", color="green", weight=3];
1004 -> 1007[label="",style="dashed", color="green", weight=3];
1005[label="primFloatEncodePower3 (primEqInt (primNegInt (Neg (Succ yx7))) (Pos Zero)) (Pos (Succ (Succ Zero))) (primNegInt (Neg (Succ yx7)))",fontsize=16,color="black",shape="box"];1005 -> 1008[label="",style="solid", color="black", weight=3];
1006[label="yx26 * (Pos (Succ Zero) * yx271)",fontsize=16,color="black",shape="triangle"];1006 -> 1009[label="",style="solid", color="black", weight=3];
1007 -> 1006[label="",style="dashed", color="red", weight=0];
1007[label="Pos (Succ Zero) * (Pos (Succ Zero) * yx270)",fontsize=16,color="magenta"];1007 -> 1010[label="",style="dashed", color="magenta", weight=3];
1007 -> 1011[label="",style="dashed", color="magenta", weight=3];
1008[label="primFloatEncodePower3 (primEqInt (Pos (Succ yx7)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (Succ yx7))",fontsize=16,color="black",shape="triangle"];1008 -> 1012[label="",style="solid", color="black", weight=3];
1009[label="primMulInt yx26 (Pos (Succ Zero) * yx271)",fontsize=16,color="burlywood",shape="box"];1203[label="yx26/Pos yx260",fontsize=10,color="white",style="solid",shape="box"];1009 -> 1203[label="",style="solid", color="burlywood", weight=9];
1203 -> 1013[label="",style="solid", color="burlywood", weight=3];
1204[label="yx26/Neg yx260",fontsize=10,color="white",style="solid",shape="box"];1009 -> 1204[label="",style="solid", color="burlywood", weight=9];
1204 -> 1014[label="",style="solid", color="burlywood", weight=3];
1010[label="Pos (Succ Zero)",fontsize=16,color="green",shape="box"];1011[label="yx270",fontsize=16,color="green",shape="box"];1012[label="primFloatEncodePower3 False (Pos (Succ (Succ Zero))) (Pos (Succ yx7))",fontsize=16,color="black",shape="box"];1012 -> 1015[label="",style="solid", color="black", weight=3];
1013[label="primMulInt (Pos yx260) (Pos (Succ Zero) * yx271)",fontsize=16,color="black",shape="box"];1013 -> 1016[label="",style="solid", color="black", weight=3];
1014[label="primMulInt (Neg yx260) (Pos (Succ Zero) * yx271)",fontsize=16,color="black",shape="box"];1014 -> 1017[label="",style="solid", color="black", weight=3];
1015[label="primFloatEncodePower2 (Pos (Succ (Succ Zero))) (Pos (Succ yx7))",fontsize=16,color="black",shape="box"];1015 -> 1018[label="",style="solid", color="black", weight=3];
1016[label="primMulInt (Pos yx260) (primMulInt (Pos (Succ Zero)) yx271)",fontsize=16,color="burlywood",shape="box"];1205[label="yx271/Pos yx2710",fontsize=10,color="white",style="solid",shape="box"];1016 -> 1205[label="",style="solid", color="burlywood", weight=9];
1205 -> 1019[label="",style="solid", color="burlywood", weight=3];
1206[label="yx271/Neg yx2710",fontsize=10,color="white",style="solid",shape="box"];1016 -> 1206[label="",style="solid", color="burlywood", weight=9];
1206 -> 1020[label="",style="solid", color="burlywood", weight=3];
1017[label="primMulInt (Neg yx260) (primMulInt (Pos (Succ Zero)) yx271)",fontsize=16,color="burlywood",shape="box"];1207[label="yx271/Pos yx2710",fontsize=10,color="white",style="solid",shape="box"];1017 -> 1207[label="",style="solid", color="burlywood", weight=9];
1207 -> 1021[label="",style="solid", color="burlywood", weight=3];
1208[label="yx271/Neg yx2710",fontsize=10,color="white",style="solid",shape="box"];1017 -> 1208[label="",style="solid", color="burlywood", weight=9];
1208 -> 1022[label="",style="solid", color="burlywood", weight=3];
1018[label="primFloatEncodePower1 (Pos (Succ yx7) >= Pos (Succ Zero)) (Pos (Succ (Succ Zero))) (Pos (Succ yx7))",fontsize=16,color="black",shape="box"];1018 -> 1023[label="",style="solid", color="black", weight=3];
1019[label="primMulInt (Pos yx260) (primMulInt (Pos (Succ Zero)) (Pos yx2710))",fontsize=16,color="black",shape="box"];1019 -> 1024[label="",style="solid", color="black", weight=3];
1020[label="primMulInt (Pos yx260) (primMulInt (Pos (Succ Zero)) (Neg yx2710))",fontsize=16,color="black",shape="box"];1020 -> 1025[label="",style="solid", color="black", weight=3];
1021[label="primMulInt (Neg yx260) (primMulInt (Pos (Succ Zero)) (Pos yx2710))",fontsize=16,color="black",shape="box"];1021 -> 1026[label="",style="solid", color="black", weight=3];
1022[label="primMulInt (Neg yx260) (primMulInt (Pos (Succ Zero)) (Neg yx2710))",fontsize=16,color="black",shape="box"];1022 -> 1027[label="",style="solid", color="black", weight=3];
1023[label="primFloatEncodePower1 (compare (Pos (Succ yx7)) (Pos (Succ Zero)) /= LT) (Pos (Succ (Succ Zero))) (Pos (Succ yx7))",fontsize=16,color="black",shape="box"];1023 -> 1028[label="",style="solid", color="black", weight=3];
1024[label="primMulInt (Pos yx260) (Pos (primMulNat (Succ Zero) yx2710))",fontsize=16,color="black",shape="box"];1024 -> 1029[label="",style="solid", color="black", weight=3];
1025[label="primMulInt (Pos yx260) (Neg (primMulNat (Succ Zero) yx2710))",fontsize=16,color="black",shape="box"];1025 -> 1030[label="",style="solid", color="black", weight=3];
1026[label="primMulInt (Neg yx260) (Pos (primMulNat (Succ Zero) yx2710))",fontsize=16,color="black",shape="box"];1026 -> 1031[label="",style="solid", color="black", weight=3];
1027[label="primMulInt (Neg yx260) (Neg (primMulNat (Succ Zero) yx2710))",fontsize=16,color="black",shape="box"];1027 -> 1032[label="",style="solid", color="black", weight=3];
1028[label="primFloatEncodePower1 (not (compare (Pos (Succ yx7)) (Pos (Succ Zero)) == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ yx7))",fontsize=16,color="black",shape="box"];1028 -> 1033[label="",style="solid", color="black", weight=3];
1029[label="Pos (primMulNat yx260 (primMulNat (Succ Zero) yx2710))",fontsize=16,color="green",shape="box"];1029 -> 1034[label="",style="dashed", color="green", weight=3];
1030[label="Neg (primMulNat yx260 (primMulNat (Succ Zero) yx2710))",fontsize=16,color="green",shape="box"];1030 -> 1035[label="",style="dashed", color="green", weight=3];
1031[label="Neg (primMulNat yx260 (primMulNat (Succ Zero) yx2710))",fontsize=16,color="green",shape="box"];1031 -> 1036[label="",style="dashed", color="green", weight=3];
1032[label="Pos (primMulNat yx260 (primMulNat (Succ Zero) yx2710))",fontsize=16,color="green",shape="box"];1032 -> 1037[label="",style="dashed", color="green", weight=3];
1033[label="primFloatEncodePower1 (not (primCmpInt (Pos (Succ yx7)) (Pos (Succ Zero)) == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ yx7))",fontsize=16,color="black",shape="box"];1033 -> 1038[label="",style="solid", color="black", weight=3];
1034[label="primMulNat yx260 (primMulNat (Succ Zero) yx2710)",fontsize=16,color="burlywood",shape="triangle"];1209[label="yx260/Succ yx2600",fontsize=10,color="white",style="solid",shape="box"];1034 -> 1209[label="",style="solid", color="burlywood", weight=9];
1209 -> 1039[label="",style="solid", color="burlywood", weight=3];
1210[label="yx260/Zero",fontsize=10,color="white",style="solid",shape="box"];1034 -> 1210[label="",style="solid", color="burlywood", weight=9];
1210 -> 1040[label="",style="solid", color="burlywood", weight=3];
1035 -> 1034[label="",style="dashed", color="red", weight=0];
1035[label="primMulNat yx260 (primMulNat (Succ Zero) yx2710)",fontsize=16,color="magenta"];1035 -> 1041[label="",style="dashed", color="magenta", weight=3];
1036 -> 1034[label="",style="dashed", color="red", weight=0];
1036[label="primMulNat yx260 (primMulNat (Succ Zero) yx2710)",fontsize=16,color="magenta"];1036 -> 1042[label="",style="dashed", color="magenta", weight=3];
1037 -> 1034[label="",style="dashed", color="red", weight=0];
1037[label="primMulNat yx260 (primMulNat (Succ Zero) yx2710)",fontsize=16,color="magenta"];1037 -> 1043[label="",style="dashed", color="magenta", weight=3];
1037 -> 1044[label="",style="dashed", color="magenta", weight=3];
1038[label="primFloatEncodePower1 (not (primCmpNat (Succ yx7) (Succ Zero) == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ yx7))",fontsize=16,color="black",shape="box"];1038 -> 1045[label="",style="solid", color="black", weight=3];
1039[label="primMulNat (Succ yx2600) (primMulNat (Succ Zero) yx2710)",fontsize=16,color="burlywood",shape="box"];1214[label="yx2710/Succ yx27100",fontsize=10,color="white",style="solid",shape="box"];1039 -> 1214[label="",style="solid", color="burlywood", weight=9];
1214 -> 1046[label="",style="solid", color="burlywood", weight=3];
1215[label="yx2710/Zero",fontsize=10,color="white",style="solid",shape="box"];1039 -> 1215[label="",style="solid", color="burlywood", weight=9];
1215 -> 1047[label="",style="solid", color="burlywood", weight=3];
1040[label="primMulNat Zero (primMulNat (Succ Zero) yx2710)",fontsize=16,color="burlywood",shape="box"];1216[label="yx2710/Succ yx27100",fontsize=10,color="white",style="solid",shape="box"];1040 -> 1216[label="",style="solid", color="burlywood", weight=9];
1216 -> 1048[label="",style="solid", color="burlywood", weight=3];
1217[label="yx2710/Zero",fontsize=10,color="white",style="solid",shape="box"];1040 -> 1217[label="",style="solid", color="burlywood", weight=9];
1217 -> 1049[label="",style="solid", color="burlywood", weight=3];
1041[label="yx2710",fontsize=16,color="green",shape="box"];1042[label="yx260",fontsize=16,color="green",shape="box"];1043[label="yx260",fontsize=16,color="green",shape="box"];1044[label="yx2710",fontsize=16,color="green",shape="box"];1045[label="primFloatEncodePower1 (not (primCmpNat yx7 Zero == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ yx7))",fontsize=16,color="burlywood",shape="box"];1218[label="yx7/Succ yx70",fontsize=10,color="white",style="solid",shape="box"];1045 -> 1218[label="",style="solid", color="burlywood", weight=9];
1218 -> 1050[label="",style="solid", color="burlywood", weight=3];
1219[label="yx7/Zero",fontsize=10,color="white",style="solid",shape="box"];1045 -> 1219[label="",style="solid", color="burlywood", weight=9];
1219 -> 1051[label="",style="solid", color="burlywood", weight=3];
1046[label="primMulNat (Succ yx2600) (primMulNat (Succ Zero) (Succ yx27100))",fontsize=16,color="black",shape="box"];1046 -> 1052[label="",style="solid", color="black", weight=3];
1047[label="primMulNat (Succ yx2600) (primMulNat (Succ Zero) Zero)",fontsize=16,color="black",shape="box"];1047 -> 1053[label="",style="solid", color="black", weight=3];
1048[label="primMulNat Zero (primMulNat (Succ Zero) (Succ yx27100))",fontsize=16,color="black",shape="box"];1048 -> 1054[label="",style="solid", color="black", weight=3];
1049[label="primMulNat Zero (primMulNat (Succ Zero) Zero)",fontsize=16,color="black",shape="box"];1049 -> 1055[label="",style="solid", color="black", weight=3];
1050[label="primFloatEncodePower1 (not (primCmpNat (Succ yx70) Zero == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx70)))",fontsize=16,color="black",shape="box"];1050 -> 1056[label="",style="solid", color="black", weight=3];
1051[label="primFloatEncodePower1 (not (primCmpNat Zero Zero == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1051 -> 1057[label="",style="solid", color="black", weight=3];
1052[label="primMulNat (Succ yx2600) (primPlusNat (primMulNat Zero (Succ yx27100)) (Succ yx27100))",fontsize=16,color="black",shape="box"];1052 -> 1058[label="",style="solid", color="black", weight=3];
1053[label="primMulNat (Succ yx2600) Zero",fontsize=16,color="black",shape="box"];1053 -> 1059[label="",style="solid", color="black", weight=3];
1054[label="primMulNat Zero (primPlusNat (primMulNat Zero (Succ yx27100)) (Succ yx27100))",fontsize=16,color="black",shape="box"];1054 -> 1060[label="",style="solid", color="black", weight=3];
1055[label="primMulNat Zero Zero",fontsize=16,color="black",shape="box"];1055 -> 1061[label="",style="solid", color="black", weight=3];
1056[label="primFloatEncodePower1 (not (GT == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx70)))",fontsize=16,color="black",shape="box"];1056 -> 1062[label="",style="solid", color="black", weight=3];
1057[label="primFloatEncodePower1 (not (EQ == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1057 -> 1063[label="",style="solid", color="black", weight=3];
1058[label="primMulNat (Succ yx2600) (primPlusNat Zero (Succ yx27100))",fontsize=16,color="black",shape="box"];1058 -> 1064[label="",style="solid", color="black", weight=3];
1059[label="Zero",fontsize=16,color="green",shape="box"];1060[label="primMulNat Zero (primPlusNat Zero (Succ yx27100))",fontsize=16,color="black",shape="box"];1060 -> 1065[label="",style="solid", color="black", weight=3];
1061[label="Zero",fontsize=16,color="green",shape="box"];1062[label="primFloatEncodePower1 (not False) (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx70)))",fontsize=16,color="black",shape="box"];1062 -> 1066[label="",style="solid", color="black", weight=3];
1063[label="primFloatEncodePower1 (not False) (Pos (Succ (Succ Zero))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1063 -> 1067[label="",style="solid", color="black", weight=3];
1064[label="primMulNat (Succ yx2600) (Succ yx27100)",fontsize=16,color="black",shape="box"];1064 -> 1068[label="",style="solid", color="black", weight=3];
1065[label="primMulNat Zero (Succ yx27100)",fontsize=16,color="black",shape="box"];1065 -> 1069[label="",style="solid", color="black", weight=3];
1066[label="primFloatEncodePower1 True (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx70)))",fontsize=16,color="black",shape="box"];1066 -> 1070[label="",style="solid", color="black", weight=3];
1067[label="primFloatEncodePower1 True (Pos (Succ (Succ Zero))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1067 -> 1071[label="",style="solid", color="black", weight=3];
1068 -> 1080[label="",style="dashed", color="red", weight=0];
1068[label="primPlusNat (primMulNat yx2600 (Succ yx27100)) (Succ yx27100)",fontsize=16,color="magenta"];1068 -> 1081[label="",style="dashed", color="magenta", weight=3];
1069[label="Zero",fontsize=16,color="green",shape="box"];1070[label="fromInt (Pos (Succ (Succ Zero))) * primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx70)) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1070 -> 1074[label="",style="solid", color="black", weight=3];
1071[label="fromInt (Pos (Succ (Succ Zero))) * primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1071 -> 1075[label="",style="solid", color="black", weight=3];
1081[label="primMulNat yx2600 (Succ yx27100)",fontsize=16,color="burlywood",shape="triangle"];1221[label="yx2600/Succ yx26000",fontsize=10,color="white",style="solid",shape="box"];1081 -> 1221[label="",style="solid", color="burlywood", weight=9];
1221 -> 1084[label="",style="solid", color="burlywood", weight=3];
1222[label="yx2600/Zero",fontsize=10,color="white",style="solid",shape="box"];1081 -> 1222[label="",style="solid", color="burlywood", weight=9];
1222 -> 1085[label="",style="solid", color="burlywood", weight=3];
1080[label="primPlusNat yx28 (Succ yx27100)",fontsize=16,color="burlywood",shape="triangle"];1223[label="yx28/Succ yx280",fontsize=10,color="white",style="solid",shape="box"];1080 -> 1223[label="",style="solid", color="burlywood", weight=9];
1223 -> 1086[label="",style="solid", color="burlywood", weight=3];
1224[label="yx28/Zero",fontsize=10,color="white",style="solid",shape="box"];1080 -> 1224[label="",style="solid", color="burlywood", weight=9];
1224 -> 1087[label="",style="solid", color="burlywood", weight=3];
1074[label="primMulFloat (fromInt (Pos (Succ (Succ Zero)))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx70)) - Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];1074 -> 1078[label="",style="solid", color="black", weight=3];
1075[label="primMulFloat (fromInt (Pos (Succ (Succ Zero)))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];1075 -> 1079[label="",style="solid", color="black", weight=3];
1084[label="primMulNat (Succ yx26000) (Succ yx27100)",fontsize=16,color="black",shape="box"];1084 -> 1090[label="",style="solid", color="black", weight=3];
1085[label="primMulNat Zero (Succ yx27100)",fontsize=16,color="black",shape="box"];1085 -> 1091[label="",style="solid", color="black", weight=3];
1086[label="primPlusNat (Succ yx280) (Succ yx27100)",fontsize=16,color="black",shape="box"];1086 -> 1092[label="",style="solid", color="black", weight=3];
1087[label="primPlusNat Zero (Succ yx27100)",fontsize=16,color="black",shape="box"];1087 -> 1093[label="",style="solid", color="black", weight=3];
1078[label="primMulFloat (primIntToFloat (Pos (Succ (Succ Zero)))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx70)) - Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];1078 -> 1088[label="",style="solid", color="black", weight=3];
1079[label="primMulFloat (primIntToFloat (Pos (Succ (Succ Zero)))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];1079 -> 1089[label="",style="solid", color="black", weight=3];
1090 -> 1080[label="",style="dashed", color="red", weight=0];
1090[label="primPlusNat (primMulNat yx26000 (Succ yx27100)) (Succ yx27100)",fontsize=16,color="magenta"];1090 -> 1096[label="",style="dashed", color="magenta", weight=3];
1091[label="Zero",fontsize=16,color="green",shape="box"];1092[label="Succ (Succ (primPlusNat yx280 yx27100))",fontsize=16,color="green",shape="box"];1092 -> 1097[label="",style="dashed", color="green", weight=3];
1093[label="Succ yx27100",fontsize=16,color="green",shape="box"];1088 -> 1124[label="",style="dashed", color="red", weight=0];
1088[label="primMulFloat (Float (Pos (Succ (Succ Zero))) (Pos (Succ Zero))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx70)) - Pos (Succ Zero)))",fontsize=16,color="magenta"];1088 -> 1125[label="",style="dashed", color="magenta", weight=3];
1089 -> 1124[label="",style="dashed", color="red", weight=0];
1089[label="primMulFloat (Float (Pos (Succ (Succ Zero))) (Pos (Succ Zero))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero)))",fontsize=16,color="magenta"];1089 -> 1126[label="",style="dashed", color="magenta", weight=3];
1096 -> 1081[label="",style="dashed", color="red", weight=0];
1096[label="primMulNat yx26000 (Succ yx27100)",fontsize=16,color="magenta"];1096 -> 1100[label="",style="dashed", color="magenta", weight=3];
1097[label="primPlusNat yx280 yx27100",fontsize=16,color="burlywood",shape="triangle"];1229[label="yx280/Succ yx2800",fontsize=10,color="white",style="solid",shape="box"];1097 -> 1229[label="",style="solid", color="burlywood", weight=9];
1229 -> 1101[label="",style="solid", color="burlywood", weight=3];
1230[label="yx280/Zero",fontsize=10,color="white",style="solid",shape="box"];1097 -> 1230[label="",style="solid", color="burlywood", weight=9];
1230 -> 1102[label="",style="solid", color="burlywood", weight=3];
1125[label="primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx70)) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1125 -> 1141[label="",style="solid", color="black", weight=3];
1124[label="primMulFloat (Float (Pos (Succ (Succ Zero))) (Pos (Succ Zero))) yx29",fontsize=16,color="burlywood",shape="triangle"];1231[label="yx29/Float yx290 yx291",fontsize=10,color="white",style="solid",shape="box"];1124 -> 1231[label="",style="solid", color="burlywood", weight=9];
1231 -> 1142[label="",style="solid", color="burlywood", weight=3];
1126[label="primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1126 -> 1143[label="",style="solid", color="black", weight=3];
1100[label="yx26000",fontsize=16,color="green",shape="box"];1101[label="primPlusNat (Succ yx2800) yx27100",fontsize=16,color="burlywood",shape="box"];1232[label="yx27100/Succ yx271000",fontsize=10,color="white",style="solid",shape="box"];1101 -> 1232[label="",style="solid", color="burlywood", weight=9];
1232 -> 1105[label="",style="solid", color="burlywood", weight=3];
1233[label="yx27100/Zero",fontsize=10,color="white",style="solid",shape="box"];1101 -> 1233[label="",style="solid", color="burlywood", weight=9];
1233 -> 1106[label="",style="solid", color="burlywood", weight=3];
1102[label="primPlusNat Zero yx27100",fontsize=16,color="burlywood",shape="box"];1234[label="yx27100/Succ yx271000",fontsize=10,color="white",style="solid",shape="box"];1102 -> 1234[label="",style="solid", color="burlywood", weight=9];
1234 -> 1107[label="",style="solid", color="burlywood", weight=3];
1235[label="yx27100/Zero",fontsize=10,color="white",style="solid",shape="box"];1102 -> 1235[label="",style="solid", color="burlywood", weight=9];
1235 -> 1108[label="",style="solid", color="burlywood", weight=3];
1141[label="primFloatEncodePower4 (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx70)) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1141 -> 1144[label="",style="solid", color="black", weight=3];
1142[label="primMulFloat (Float (Pos (Succ (Succ Zero))) (Pos (Succ Zero))) (Float yx290 yx291)",fontsize=16,color="black",shape="box"];1142 -> 1145[label="",style="solid", color="black", weight=3];
1143[label="primFloatEncodePower4 (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1143 -> 1146[label="",style="solid", color="black", weight=3];
1105[label="primPlusNat (Succ yx2800) (Succ yx271000)",fontsize=16,color="black",shape="box"];1105 -> 1111[label="",style="solid", color="black", weight=3];
1106[label="primPlusNat (Succ yx2800) Zero",fontsize=16,color="black",shape="box"];1106 -> 1112[label="",style="solid", color="black", weight=3];
1107[label="primPlusNat Zero (Succ yx271000)",fontsize=16,color="black",shape="box"];1107 -> 1113[label="",style="solid", color="black", weight=3];
1108[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];1108 -> 1114[label="",style="solid", color="black", weight=3];
1144[label="primFloatEncodePower3 (Pos (Succ (Succ yx70)) - Pos (Succ Zero) == Pos Zero) (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx70)) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1144 -> 1147[label="",style="solid", color="black", weight=3];
1145[label="Float (Pos (Succ (Succ Zero)) * yx290) (Pos (Succ Zero) * yx291)",fontsize=16,color="green",shape="box"];1145 -> 1148[label="",style="dashed", color="green", weight=3];
1145 -> 1149[label="",style="dashed", color="green", weight=3];
1146[label="primFloatEncodePower3 (Pos (Succ Zero) - Pos (Succ Zero) == Pos Zero) (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1146 -> 1150[label="",style="solid", color="black", weight=3];
1111[label="Succ (Succ (primPlusNat yx2800 yx271000))",fontsize=16,color="green",shape="box"];1111 -> 1117[label="",style="dashed", color="green", weight=3];
1112[label="Succ yx2800",fontsize=16,color="green",shape="box"];1113[label="Succ yx271000",fontsize=16,color="green",shape="box"];1114[label="Zero",fontsize=16,color="green",shape="box"];1147[label="primFloatEncodePower3 (primEqInt (Pos (Succ (Succ yx70)) - Pos (Succ Zero)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx70)) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1147 -> 1151[label="",style="solid", color="black", weight=3];
1148[label="Pos (Succ (Succ Zero)) * yx290",fontsize=16,color="black",shape="box"];1148 -> 1152[label="",style="solid", color="black", weight=3];
1149[label="Pos (Succ Zero) * yx291",fontsize=16,color="black",shape="box"];1149 -> 1153[label="",style="solid", color="black", weight=3];
1150[label="primFloatEncodePower3 (primEqInt (Pos (Succ Zero) - Pos (Succ Zero)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];1150 -> 1154[label="",style="solid", color="black", weight=3];
1117 -> 1097[label="",style="dashed", color="red", weight=0];
1117[label="primPlusNat yx2800 yx271000",fontsize=16,color="magenta"];1117 -> 1120[label="",style="dashed", color="magenta", weight=3];
1117 -> 1121[label="",style="dashed", color="magenta", weight=3];
1151[label="primFloatEncodePower3 (primEqInt (primMinusInt (Pos (Succ (Succ yx70))) (Pos (Succ Zero))) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusInt (Pos (Succ (Succ yx70))) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];1151 -> 1155[label="",style="solid", color="black", weight=3];
1152[label="primMulInt (Pos (Succ (Succ Zero))) yx290",fontsize=16,color="burlywood",shape="box"];1237[label="yx290/Pos yx2900",fontsize=10,color="white",style="solid",shape="box"];1152 -> 1237[label="",style="solid", color="burlywood", weight=9];
1237 -> 1156[label="",style="solid", color="burlywood", weight=3];
1238[label="yx290/Neg yx2900",fontsize=10,color="white",style="solid",shape="box"];1152 -> 1238[label="",style="solid", color="burlywood", weight=9];
1238 -> 1157[label="",style="solid", color="burlywood", weight=3];
1153[label="primMulInt (Pos (Succ Zero)) yx291",fontsize=16,color="burlywood",shape="box"];1239[label="yx291/Pos yx2910",fontsize=10,color="white",style="solid",shape="box"];1153 -> 1239[label="",style="solid", color="burlywood", weight=9];
1239 -> 1158[label="",style="solid", color="burlywood", weight=3];
1240[label="yx291/Neg yx2910",fontsize=10,color="white",style="solid",shape="box"];1153 -> 1240[label="",style="solid", color="burlywood", weight=9];
1240 -> 1159[label="",style="solid", color="burlywood", weight=3];
1154[label="primFloatEncodePower3 (primEqInt (primMinusInt (Pos (Succ Zero)) (Pos (Succ Zero))) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusInt (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];1154 -> 1160[label="",style="solid", color="black", weight=3];
1120[label="yx2800",fontsize=16,color="green",shape="box"];1121[label="yx271000",fontsize=16,color="green",shape="box"];1155[label="primFloatEncodePower3 (primEqInt (primMinusNat (Succ (Succ yx70)) (Succ Zero)) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusNat (Succ (Succ yx70)) (Succ Zero))",fontsize=16,color="black",shape="box"];1155 -> 1161[label="",style="solid", color="black", weight=3];
1156[label="primMulInt (Pos (Succ (Succ Zero))) (Pos yx2900)",fontsize=16,color="black",shape="box"];1156 -> 1162[label="",style="solid", color="black", weight=3];
1157[label="primMulInt (Pos (Succ (Succ Zero))) (Neg yx2900)",fontsize=16,color="black",shape="box"];1157 -> 1163[label="",style="solid", color="black", weight=3];
1158[label="primMulInt (Pos (Succ Zero)) (Pos yx2910)",fontsize=16,color="black",shape="box"];1158 -> 1164[label="",style="solid", color="black", weight=3];
1159[label="primMulInt (Pos (Succ Zero)) (Neg yx2910)",fontsize=16,color="black",shape="box"];1159 -> 1165[label="",style="solid", color="black", weight=3];
1160[label="primFloatEncodePower3 (primEqInt (primMinusNat (Succ Zero) (Succ Zero)) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusNat (Succ Zero) (Succ Zero))",fontsize=16,color="black",shape="box"];1160 -> 1166[label="",style="solid", color="black", weight=3];
1161[label="primFloatEncodePower3 (primEqInt (primMinusNat (Succ yx70) Zero) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusNat (Succ yx70) Zero)",fontsize=16,color="black",shape="box"];1161 -> 1167[label="",style="solid", color="black", weight=3];
1162[label="Pos (primMulNat (Succ (Succ Zero)) yx2900)",fontsize=16,color="green",shape="box"];1162 -> 1168[label="",style="dashed", color="green", weight=3];
1163[label="Neg (primMulNat (Succ (Succ Zero)) yx2900)",fontsize=16,color="green",shape="box"];1163 -> 1169[label="",style="dashed", color="green", weight=3];
1164[label="Pos (primMulNat (Succ Zero) yx2910)",fontsize=16,color="green",shape="box"];1164 -> 1170[label="",style="dashed", color="green", weight=3];
1165[label="Neg (primMulNat (Succ Zero) yx2910)",fontsize=16,color="green",shape="box"];1165 -> 1171[label="",style="dashed", color="green", weight=3];
1166[label="primFloatEncodePower3 (primEqInt (primMinusNat Zero Zero) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusNat Zero Zero)",fontsize=16,color="black",shape="box"];1166 -> 1172[label="",style="solid", color="black", weight=3];
1167 -> 1008[label="",style="dashed", color="red", weight=0];
1167[label="primFloatEncodePower3 (primEqInt (Pos (Succ yx70)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (Succ yx70))",fontsize=16,color="magenta"];1167 -> 1173[label="",style="dashed", color="magenta", weight=3];
1168[label="primMulNat (Succ (Succ Zero)) yx2900",fontsize=16,color="burlywood",shape="triangle"];1242[label="yx2900/Succ yx29000",fontsize=10,color="white",style="solid",shape="box"];1168 -> 1242[label="",style="solid", color="burlywood", weight=9];
1242 -> 1174[label="",style="solid", color="burlywood", weight=3];
1243[label="yx2900/Zero",fontsize=10,color="white",style="solid",shape="box"];1168 -> 1243[label="",style="solid", color="burlywood", weight=9];
1243 -> 1175[label="",style="solid", color="burlywood", weight=3];
1169 -> 1168[label="",style="dashed", color="red", weight=0];
1169[label="primMulNat (Succ (Succ Zero)) yx2900",fontsize=16,color="magenta"];1169 -> 1176[label="",style="dashed", color="magenta", weight=3];
1170[label="primMulNat (Succ Zero) yx2910",fontsize=16,color="burlywood",shape="triangle"];1245[label="yx2910/Succ yx29100",fontsize=10,color="white",style="solid",shape="box"];1170 -> 1245[label="",style="solid", color="burlywood", weight=9];
1245 -> 1177[label="",style="solid", color="burlywood", weight=3];
1246[label="yx2910/Zero",fontsize=10,color="white",style="solid",shape="box"];1170 -> 1246[label="",style="solid", color="burlywood", weight=9];
1246 -> 1178[label="",style="solid", color="burlywood", weight=3];
1171 -> 1170[label="",style="dashed", color="red", weight=0];
1171[label="primMulNat (Succ Zero) yx2910",fontsize=16,color="magenta"];1171 -> 1179[label="",style="dashed", color="magenta", weight=3];
1172[label="primFloatEncodePower3 (primEqInt (Pos Zero) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos Zero)",fontsize=16,color="black",shape="box"];1172 -> 1180[label="",style="solid", color="black", weight=3];
1173[label="yx70",fontsize=16,color="green",shape="box"];1174[label="primMulNat (Succ (Succ Zero)) (Succ yx29000)",fontsize=16,color="black",shape="box"];1174 -> 1181[label="",style="solid", color="black", weight=3];
1175[label="primMulNat (Succ (Succ Zero)) Zero",fontsize=16,color="black",shape="box"];1175 -> 1182[label="",style="solid", color="black", weight=3];
1176[label="yx2900",fontsize=16,color="green",shape="box"];1177[label="primMulNat (Succ Zero) (Succ yx29100)",fontsize=16,color="black",shape="box"];1177 -> 1183[label="",style="solid", color="black", weight=3];
1178[label="primMulNat (Succ Zero) Zero",fontsize=16,color="black",shape="box"];1178 -> 1184[label="",style="solid", color="black", weight=3];
1179[label="yx2910",fontsize=16,color="green",shape="box"];1180[label="primFloatEncodePower3 True (Pos (Succ (Succ Zero))) (Pos Zero)",fontsize=16,color="black",shape="box"];1180 -> 1185[label="",style="solid", color="black", weight=3];
1181 -> 1097[label="",style="dashed", color="red", weight=0];
1181[label="primPlusNat (primMulNat (Succ Zero) (Succ yx29000)) (Succ yx29000)",fontsize=16,color="magenta"];1181 -> 1186[label="",style="dashed", color="magenta", weight=3];
1181 -> 1187[label="",style="dashed", color="magenta", weight=3];
1182[label="Zero",fontsize=16,color="green",shape="box"];1183 -> 1097[label="",style="dashed", color="red", weight=0];
1183[label="primPlusNat (primMulNat Zero (Succ yx29100)) (Succ yx29100)",fontsize=16,color="magenta"];1183 -> 1188[label="",style="dashed", color="magenta", weight=3];
1183 -> 1189[label="",style="dashed", color="magenta", weight=3];
1184[label="Zero",fontsize=16,color="green",shape="box"];1185[label="fromDouble (Double (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];1185 -> 1190[label="",style="solid", color="black", weight=3];
1186 -> 1081[label="",style="dashed", color="red", weight=0];
1186[label="primMulNat (Succ Zero) (Succ yx29000)",fontsize=16,color="magenta"];1186 -> 1191[label="",style="dashed", color="magenta", weight=3];
1186 -> 1192[label="",style="dashed", color="magenta", weight=3];
1187[label="Succ yx29000",fontsize=16,color="green",shape="box"];1188 -> 1081[label="",style="dashed", color="red", weight=0];
1188[label="primMulNat Zero (Succ yx29100)",fontsize=16,color="magenta"];1188 -> 1193[label="",style="dashed", color="magenta", weight=3];
1188 -> 1194[label="",style="dashed", color="magenta", weight=3];
1189[label="Succ yx29100",fontsize=16,color="green",shape="box"];1190[label="doubleToFloat (Double (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];1190 -> 1195[label="",style="solid", color="black", weight=3];
1191[label="yx29000",fontsize=16,color="green",shape="box"];1192[label="Succ Zero",fontsize=16,color="green",shape="box"];1193[label="yx29100",fontsize=16,color="green",shape="box"];1194[label="Zero",fontsize=16,color="green",shape="box"];1195[label="Float (Pos (Succ Zero)) (Pos (Succ Zero))",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                          ↳ QDP

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yx2800), Succ(yx271000)) → new_primPlusNat(yx2800, yx271000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(yx2800), Succ(yx271000)) → new_primPlusNat(yx2800, yx271000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yx26000), yx27100) → new_primMulNat(yx26000, yx27100)

From the DPs we obtained the following set of size-change graphs:

new_primMulNat(Succ(yx26000), yx27100) → new_primMulNat(yx26000, yx27100)
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_primFloatEncodePower3(Succ(yx70)) → new_primFloatEncodePower3(yx70)

From the DPs we obtained the following set of size-change graphs:

new_primFloatEncodePower3(Succ(yx70)) → new_primFloatEncodePower3(yx70)
The graph contains the following edges 1 > 1

power	vw 0	= 1.0
power	x vx@(y+1)	= fromInt x * power x y
power	x y	= 1.0 / power x (`negate` y)

power	vw xw	= power4 vw xw
power	x vx	= power2 x vx
power	x y	= power0 x y

power1	True x vx	= fromInt x * power x (vx - 1)
power1	wx wy wz	= power0 wy wz

power4	vw xw	= power3 (xw == 0) vw xw
power4	yu yv	= power2 yu yv

primFloatEncodePower4	vw xw	= primFloatEncodePower3 (xw == 0) vw xw
primFloatEncodePower4	yu yv	= primFloatEncodePower2 yu yv

primFloatEncodePower1	True x vx	= fromInt x * primFloatEncodePower x (vx - 1)
primFloatEncodePower1	wx wy wz	= primFloatEncodePower0 wy wz

primFloatEncodePower3	True vw xw	= 1.0
primFloatEncodePower3	xx xy xz	= primFloatEncodePower2 xy xz

primFloatEncodePower	vw xw	= primFloatEncodePower4 vw xw
primFloatEncodePower	x vx	= primFloatEncodePower2 x vx
primFloatEncodePower	x y	= primFloatEncodePower0 x y

primFloatEncodePower2	x vx	= primFloatEncodePower1 (vx >= 1) x vx
primFloatEncodePower2	xu xv	= primFloatEncodePower0 xu xv